The Lean proof assistant

Abstract: There are several software that can be used to formalize mathematics, called proof assistants. One of the most used today by mathematician is Lean: it has a huge library of already formalized mathematics, Mathlib, that allows to treat serious mathematics almost as we do ``on the blackboard''. I will explain the basics of Lean and mathlib, showing their how far we can go using them. If time permits, I will briefly mention some limitations and how they will be solved in the (hopefully near) future.

Mathematics

Audience: undergraduates

An introduction to proof assistants: a mini course about mathematical formalization

Series comments: The goal of this mini-course is to give an introduction to formalization of mathematics. I will explain what formalizing mathematics means and why it is interesting and useful for people interested in "standard" mathematics. I will show how this is done in practice using Lean, one of the several proof assistants available today. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.